\begin{tabbing}
$\forall$$A$:Type, $f$:($A$$\rightarrow$($A$ + Top)).
\\[0ex]SWellFounded(p{-}graph($A$;$f$)($y$,$x$))
\\[0ex]$\Rightarrow$ \=($\forall$$x$:$A$.\+
\\[0ex]$\exists$\=$n$:$\mathbb{N}$\+
\\[0ex](($\uparrow$can{-}apply($f$\^{}$n$;$x$))
\\[0ex]c$\wedge$ \=(final{-}iterate($f$;$x$) = do{-}apply($f$\^{}$n$;$x$) $\in$ $A$\+
\\[0ex]\& ($\neg$($\uparrow$can{-}apply($f$;final{-}iterate($f$;$x$)))))))
\-\-\-
\end{tabbing}